This paper extends the fibrational approach to induction and coinductionpioneered by Hermida and Jacobs, and developed by the current authors, in twokey directions. First, we present a dual to the sound induction rule forinductive types that we developed previously. That is, we present a soundcoinduction rule for any data type arising as the carrier of the finalcoalgebra of a functor, thus relaxing Hermida and Jacobs' restriction topolynomial functors. To achieve this we introduce the notion of a quotientcategory with equality (QCE) that i) abstracts the standard notion of afibration of relations constructed from a given fibration; and ii) plays a rolein the theory of coinduction dual to that played by a comprehension categorywith unit (CCU) in the theory of induction. Secondly, we show that inductiveand coinductive indexed types also admit sound induction and coinduction rules.Indexed data types often arise as carriers of initial algebras and finalcoalgebras of functors on slice categories, so we give sufficient conditionsunder which we can construct, from a CCU (QCE) U:E \rightarrow B, a fibrationwith base B/I that models indexing by I and is also a CCU (resp., QCE). Wefinish the paper by considering the more general case of sound induction andcoinduction rules for indexed data types when the indexing is itself given by afibration.
展开▼
